00100	COMMENT ⊗   VALID 00003 PAGES
00200	C REC  PAGE   DESCRIPTION
00300	C00001 00001
00400	C00002 00002	(This file is KNOW.NOT[226,JMC] and is being revised.)
00500	C00017 00003	Hintikka, Jaako (1962) Knowledge and belief: an introduction
00600	C00018 ENDMK
00700	C⊗;
     

00100	(This file is KNOW.NOT[226,JMC] and is being revised.)
00200	
00300	
00400	SOME FORMALISM FOR KNOWLEDGE AND BELIEF
00500	
00600	by John McCarthy
00700	
00800	
00900		Here are some formalisms that we propose to use to treat knowledge.
01000	The approach is somewhat different from that of (McCarthy and Hayes 1969),
01100	but the result formalism of that paper is used and some of the problems
01200	treated are the same.
01300	We shall deal with a certain class of symbolic expressions not yet determined
01400	but which will contain expressions like
01500	
01600		telephone-number(Mike)
01700	
01800	or in LISP notation
01900	
02000		(TELEPHONE-NUMBER MIKE).
02100	
02200	In these notes, we shall often use an informal notation, but we expect
02300	to use LISP S-expressions as the internal notation of some actual proof
02400	checker or reasoning program.
02500	
02600		We are interested in expressions that have values and
02700	
02800		value[(TELEPHONE-NUMBER MIKE)]
02900	
03000	denotes the value of (TELEPHONE-NUMBER MIKE).  
03100	A reflection principle will be assumed to exist in the logic that will
03200	generate assertions like
03300	
03400		value[(TELEPHONE-NUMBER MIKE)] = telephone-number(Mike).
03500	
03600		Such a reflection principle is like those in metamathematics that
03700	generate assertions like
03800	
03900		true["It is snowing"] ≡ It is snowing,
04000	
04100	but our form is more general and the greater generality seems to be required
04200	for the applications.
04300	
04400		We may later have to give value two arguments, the second being an
04500	environment or possible world or situation or something like that but for
04600	the time being we will not do this.
04700	
04800		We will treat knowledge and belief by introducing 
04900	value(<person>,<expression>,<situation>) where value(p,e,s) is the
05000	value that p ascribes to e in s.  Thus
05100	
05200		value[John,(TELEPHONE-NUMBER MIKE),S0]
05300	
05400	is the value that John ascribes to Mike's telephone number in situation S0.
05500	Note that the situation argument refers to the situation in which the
05600	ascription occurs not some situation referred to in the expression.
05700	
05800		With this notation we can say that John believs Mikes telephone number
05900	is 321-1234 by writing
06000	
06100		value[John,(TELEPHONE-NUMBER MIKE),S0] = "321-1234"
06200	
06300	where the number in quotes might have to be written
06400	(3 2 1 - 1 2 3 4) in an actual LISP implementation.
06500	
06600		We can say that John knows Mike's telephone number without asserting
06700	what this telephone number is by writing
06800	
06900		value[John,(TELEPHONE-NUMBER MIKE),S0] = telephone-number[Mike]
07000	
07100	or
07200	
07300		value[John,(TELEPHONE-NUMBER MIKE),S0] = value[(TELEPHONE-NUMBER MIKE)].
07400	
07500	These two sentences are equivalent by the reflection principle, and one
07600	might therefore suppose that the value notation is superfluous.  Its
07700	necessity arises as soon as we want to introduce quantifiers.
07800	
07900		Namely, we define knowing by the axiom
08000	
08100		(∀ p e s)(knows(p,e,s) ≡ value(p,e,s) = value(e),
08200	
08300	and without the function value we couldn't write this definition.
08400	
08500		Now suppose we want to assert that the act of looking up someone's number
08600	in the book results in one's knowing the number.  We first introduce the
08700	notion of name as a function applied to people.  Naturally, we have
08800	
08900		name[Mike] = MIKE
09000	
09100	where we shall regard MIKE as a LISP atom although we may later have to switch
09200	to a notation in which it is a string of characters.  Our idea is that looking
09300	up is an action performed on names and not on people.  We also have to use
09400	the LISP function subst[x,y,z] which denotes the result of substituting the
09500	expression x for each occurrence  of the expression y in the expression z.
09600	
09700		Now we write
09800	
09900		(∀ p q s)(value[p,subst[name[q],Q,(TELEPHONE-NUMBER Q)],
10000				result[p,lookup[name[q]],s]]
10100		= telephone-number[q]).
10200	
10300	We could write simply (TELEPHONE-NUMBER name[q]) instead of "subst[...] provided
10400	we understand that (TELEPHONE-NUMBER name[q]) stands for the result of
10500	making a list out of TELEPHONE-NUMBER and whatever name[q] turns out to
10600	be in the particular case.  In our scheme of things, to write
10700	(TELEPHONE-NUMBER q) would be incorrect because this would be trying to put
10800	a person into an S-expression where we can only put the name of a person.
10900	
11000		
11100	Remarks:
11200	
11300		1. Tentatively, we shall treat only cases where the value of the
11400	expressions considered is undefined or a symbolic expression or a number.
11500	This is to avoid having to worry about "Mike knows John" wherein
11600	value[Mike,denotation[JOHN],s] would have to be a person, and this seems
11700	difficult to treat.
11800	
11900		2. The language in which the expressions are written is not
12000	necessarily that of the person to whom values are being ascribed.  Thus
12100	we want to say , value[Mikhail,(TELEPHONE-NUMBER ANDREI),S] = 65-03-52
12200	without assuming that Mikhail speaks English or LISP.  Indeed, we
12300	may want to say
12400	
12500		value[Fido,"hand with ball",S] = LEFT
12600	
12700	in order to assert that Fido thinks the ball is in the left hand
12800	without assuming that Fido uses language.  Naturally, in this
12900	case we need to be especially careful about what we allow
13000	ourselves to deduce from the assertion about what Fido believes.
13100	
13200		3. Metamathematical work concerning knowledge and belief has
13300	mainly concerned knowledge of propositions.  Expressing this in terms
13400	of knowledge and belief of sentences, i.e. symbolic expressions
13500	representing the propositions, is one of the options that has been
13600	considered.  The more popular option is to regard knowledge or belief
13700	as a modal operator, because they resemble the operators of modal logic
13800	in some of their properties.  I don't know any work in mathematical
13900	logic that follows the same line as this paper in letting the operand
14000	of belief be a general expression.
14100	
14200		Kaplan and Montague (1960) and Montague (1963) discuss
14300	axiomatizations of knowledge and derive contradictions from a set
14400	of very plausible axioms.  We intend to avoid these contradictions
14500	by restricting what expressions can be operands of the value function,
14600	we don't yet know what restrictions to impose.
14700	
14800		4. Most logicians and philosophers who have considered the matter
14900	seem to believe that modal logic is the appropriate formalism for
15000	expressing facts about knowledge and belief.  It seems to me that the
15100	arguments presume that at most one of the proposed formalisms is right.
15200	It seems evident to me, however, that whatever may be most convenient
15300	in some general sense, making the object of belief an expression is an
15400	option.  Namely, there is some relation between Fido and "the hand
15500	holding the ball", and we are at liberty to study it if we want to.
15600	
15700		My opinion that this formalism will work out best for AI purposes,
15800	however, is admittedly just a bet.  It is just that I wish to
15900	avoid accusations that I don't understand the true nature of knowledge
16000	just because I choose to study this relation rather than some other.
16100	
16110		5. There is a temptation to identify knowledge with true
16120	belief, and this can be expressed by obvious axioms both in the
16130	case of knowledge of an assertion and knowledge of the value of
16140	an expression.  Many philosophers have doubts about this identification,
16150	because someone might believe that McGovern won the election in
16160	1972 and deduce from that that Nixon is not President in October
16170	1974.  He believes that Nixon is not President and that belief
16180	is true but one is hesitant to say that he knows that Nixon is
16190	not President.  Philosophers have suggested that knowledge is
16191	properly founded true belief.  My current idea is to call a true
16192	belief knowledge if the belief system is consistent (or at least
16193	the part of the system connected to the belief is consistent if
16194	we can work out compartmented belief systems such that an
16195	inconsistency in one compartment doesn't spoil the whole) and
16196	if eliminating false beliefs and adding additonal true beliefs
16197	would not cause the person to stop believing the sentence.  Thus
16198	knowledge is true belief that won't go away when the belief
16199	system is improved.
16200	
16201	
16300	LOGIC OF BELIEF AND KNOWLEDGE
16400	
16500		Opportunities and difficulties arise when we attempt to deduce
16600	from assertions that a person believes one thing to an assertion that
16700	he believes something else.  These arise both from the practical AI
16800	point of view and from the logical point of view.  Let's begin with
16900	the AI point of view.
17000	
17100		Suppose I tell you that Smith is in New York.  Then I expect
17200	you to know that Smith is not in California.  Therefore, our intuitive
17300	notion of knowledge and belief expects certain consequences of things
17400	believed also to be believed.  However, I obviously can't expect you
17500	to believe all consequences of your beliefs.  A robot that
17600	has to determine what people will do in response to what it tells
17700	them will also have to reason from beliefs to beliefs.  Pending the
17800	develpment of a notion of "obvious consequence", it may be best to
17900	use axioms in which all consequences of beliefs are believed.
18000	
18100		Montague and Kaplan (1960) discuss the following axiom
18200	schemes for knowledge of sentences:
18300	
18400		S1. K[p'] ⊃ p
18500	
18600		S2. K[[K[p'] ⊃ p]']
18700	
18800		S3. [I[p',q'] ∧ K[p']] ⊃ K[q'].
18900	
19000	Here p and q are sentences and p' denotes the written form of p.  Thus
19100	S1 asserts that if something is known, it is so, S2 asserts that this
19200	principle is known, and S3 asserts that if q is deducible from p and p
19300	is known, then q is known.
19400	
19500		They show that if a first order language contains elementary syntax
19600	and all instances of these schemata, then it is inconsistent.  Montague (1963)
19700	discusses these matters further.
19800	
19900		We plan to get out of the difficulty by putting some restriction on
20000	the kind of sentences that can be known or believed.  These restrictions
20100	will involve the way the knowledge operator and quantifiers can occur, but
20200	I don't have a proposal yet.  Actually, the axioms and the restrictions will
20300	take a different form, because we need the value[p,e,s] formalism, but all
20400	the difficulties noted by Kaplan and Montague will arise, because the value
20500	formalism includes theirs.
20600	
20700		A natural first axiom to consider in the "value" formalism is
20800	
20900		value[p,(f x),s] = value[p,f,x][value[p,x,s]].
21000	
21100	This asserts that the value p gives for f(x) is the value he gives for f
21200	applied to the value he gives for x.
21300	
21400		As stated, it seems that the principle is incorrect, because
21500	a person could have a value for f(x) without having a value for f
21600	or a value for x.  Therefore, we should rewrite it as
21700	
21800		value[p,f,s] ≠ UU ∧ value[p,x,s] ≠ UU
21900				⊃
22000		value[p,(f x),s] = value[p,f,x][value[p,x,s]].
22100	
22200		This could be criticised on the grounds that we should distinguish
22300	between a person not having a value for an expression and his belief that
22400	its value is undefined.  We shall have to revise this.
22500	
22600		Another issue is whether having a value for f(x) for all x implies
22700	that one has a value for f.  Probably not.
22800	
     

00100	Hintikka, Jaako (1962) Knowledge and belief: an introduction
00200	to the logic of the two notions. New York: Cornell University
00300	Press.
00400	
00500	Kaplan, David and Montague, Richard (1960).  A paradox regained.
00600	Notre Dame Journal of Formal Logic, vol. 1, pp. 79-90.
00700	
00800	McCarthy, John and Hayes, Patrick (1969).  Some philosophical
00900	problems from the standpoint of artificial intelligence.  in
01000	Machine Intelligence 4, Edinburgh University Press, pp. 463-502.
01100	
01200	Montague, Richard (1963). Syntactical treatments of Modality, with
01300	corollaries on reflexion principles and finite axiomatizability.
01400	Acta Philosophica Fennica, vol.  , pp. 153-167.